$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)).
\\[0ex](causal{-}predecessor(${\it es}$;$p$) \& p{-}inject(E;E;$p$))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:E. same{-}thread(${\it es}$;$p$;$e$;${\it e'}$) $\Rightarrow$ (($e$ $p$$<$ ${\it e'}$ $\vee$ ($e$ = ${\it e'}$)) $\vee$ ${\it e'}$ $p$$<$ $e$))